r:Rng.
Assoc(|r|;+r)
& Ident(|r|;+r;0)
& Inverse(|r|;+r;0;-r)
& Assoc(|r|;*)
& Ident(|r|;*;1)
& BiLinear(|r|;+r;*)
& IsEqFun(|r|;=) 

latex

Up	rings 1
Definitions of Statement	IsRing(T;plus;zero;neg;times;one), Rng
Definitions	t  T, x:A. B(x), P & Q, Rng, IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsRing(T;plus;zero;neg;times;one)
Lemmas	rng wf, rng properties